PACKAGE BODY Sort IS

   PROCEDURE SelSort (A: IN IntArray; B: OUT IntArray) IS
      N: Integer := A'Last;
      Links: Integer := A'First;
      I: Integer;
      Min: Integer;
      T: IntArray(A'First..A'Last) := A;
   BEGIN
      --#PRE: A = T AND Links = A'First AND N = A'Last
      --#BOUND: (N-Links)+1
      --#INV: Links <= N
      WHILE Links <= N LOOP
         Min := Links;
         I := Links+1;
         --#BOUND: (N-I)+1
         --#INV: I <= N+1 AND I >= (Links+1)
         WHILE I <= N LOOP
            IF(T(I) < T(Min)) THEN
               Min := I;
            END IF;
            I := I+1;
         END LOOP;
         B(Min) := T(Links);
         B(Links) := T(Min);
         T(Min) := B(Min);
         T(Links) := B(Links);
         Links := Links+1;
      END LOOP;
      --#POST: Links = N+1
   END SelSort;

   PROCEDURE FindMaxIndex (A: IN IntArray; I: OUT Integer) IS
      J: Integer := A'First;
      H: Integer := 0;
   BEGIN
      --#PRE: J = A'First AND H = 0
      --#BOUND: (A'Last-1)+1
      --#INV: J <= (A'Last+1)
      WHILE J <= A'Last LOOP
         IF A(J) > H THEN
            H := A(J);
            I := J;
         END IF;
         J := J+1;
      END LOOP;
      --#POST: J = (A'Last+1) AND forall X in [A'first..A'last]: A(I) >= A(X)
   END FindMaxIndex;

   PROCEDURE MaxSort (A: IN IntArray; B: OUT IntArray) IS
      I: Integer := A'Last;
      J: Integer := 1;
      Tmp: IntArray (A'First..A'Last) := A;
   BEGIN
      --#PRE: I = A'Last AND J = 1 AND Tmp = A
      --#BOUND: I
      --#INV: I >= (A'First-1)
      WHILE I >= A'First LOOP
         FindMaxIndex(Tmp, J);
         B(I) := Tmp(J);
         Tmp(J) := 0;
         I := I-1;
      END LOOP;
      --#POST: I = (A'First-1)
   END MaxSort;

   PROCEDURE AnzXin (A: IN IntArray; X: IN Integer; Y: OUT Integer) IS
      I: Integer := A'First;
   BEGIN
      --#PRE: I = A'First
      Y := 0;
      --#BOUND: (A'Last-I)+1
      --#INV: I <= (A'Last+1)
      WHILE I <= A'Last LOOP
         IF A(I) = X THEN
            Y := Y+1;
         END IF;
         I := I+1;
      END LOOP;
      --#POST: I = (A'Last+1)
   END AnzXin;

   PROCEDURE IsPerm (A, B: IN IntArray; W: OUT Integer) IS
      I: Integer := A'First;
   BEGIN
      --#PRE: I = A'First
      W := 1;
      --#FALL: I = A'First AND W = 1
      IF A'Last /= B'Last THEN
         W := 0;
      ELSE
         --#BOUND: (A'Last-I)+1
         --#INV: I <= (A'Last+1) AND FORALL j IN [A'First..A'Last]: AnzXin(A, A(j)) /= AnzXin(B, A(j)) 
         WHILE I <= A'Last LOOP
            AnzXin(A, A(I), TA);
            AnzXin(B, A(I), TB);
            IF TA /= TB THEN
               W := 0;
            END IF;
            I := I+1;
         END LOOP;
      END IF;
      --#POST: I = (A'Last+1)
   END IsPerm;

   PROCEDURE IsPerm2 (A,B: IN IntArray; W: OUT Integer) IS
   BEGIN
      IsPerm(A,B,W);
   END IsPerm2;

END Sort;